NIL 
EVAL-AWAITS 
NIL 1 2
1 ¬on(B,C,R(puton(A,B),R(puton(x,C),R(puton(C,T),S0))));3 4
2 on(B,C,R(puton(A,x),R(puton(B,C),R(puton(y,T),S0))));5 6
3 ¬(on(A,B,x)∧on(B,C,x));THM
4 on(A,B,R(puton(A,B),R(puton(x,C),R(puton(C,T),S0))));7 8
5 x = B∨on(B,C,R(puton(x,y),R(puton(B,C),R(puton(z,T),S0))));9 10
6 ¬A = B;AXIOM
7 clear(x,R(puton(y,C),R(puton(z,T),S0)))⊃on(x,B,R(puton(x,B),R(puton(y,C),R(puton(z,T),S0))));11 22
8 clear(A,R(puton(x,C),R(puton(C,T),S0)));13 14
9 on(x,y,s)⊃z = x∨on(x,y,R(puton(z,u),s));AXIOM
10 on(B,C,R(puton(B,C),R(puton(x,T),S0)));15 25
11 clear(B,R(puton(x,C),R(puton(y,T),S0)));17 18
13 A = y∨clear(A,R(puton(x,y),R(puton(C,T),S0)));19 40
14 ¬A = C;AXIOM
15 clear(x,R(puton(y,T),S0))⊃on(x,C,R(puton(x,C),R(puton(y,T),S0)));21 22
17 B = y∨clear(B,R(puton(x,y),R(puton(z,T),S0)));25 40
18 ¬B = C;AXIOM
19 clear(A,R(puton(C,T),S0));27 28
21 clear(C,R(puton(x,T),S0));29 30
22 clear(x,z)∧clear(y,z)⊃on(x,y,R(puton(x,y),z));AXIOM
25 clear(B,R(puton(x,T),S0));33 34
27 x = A∨clear(A,R(puton(C,x),S0));35 36
28 ¬T = A;AXIOM
29 C = y∨clear(C,R(puton(x,y),S0));37 40
30 ¬C = T;AXIOM
33 B = y∨clear(B,R(puton(x,y),S0));39 40
34 ¬B = T;AXIOM
35 on(y,x,u)⊃z = x∨clear(x,R(puton(y,z),u));AXIOM
36 on(C,A,S0);AXIOM
37 clear(C,S0);AXIOM
39 clear(B,S0);AXIOM
40 clear(x,u)⊃x = z∨clear(x,R(puton(y,z),u));AXIOM
NIL 
EVAL-AWAITS